YES 1.123
↳ HASKELL
↳ IFR
((union :: [()] -> [()] -> [()]) :: [()] -> [()] -> [()]) |
import qualified Maybe import qualified Prelude |
|||||||||||||||||||||||||||
deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
|
|||||||||||||||||||||||||||
elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
|
|||||||||||||||||||||||||||
nubBy :: (a -> a -> Bool) -> [a] -> [a]
|
|||||||||||||||||||||||||||
union :: Eq a => [a] -> [a] -> [a]
|
|||||||||||||||||||||||||||
unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
|
import qualified List import qualified Prelude |
if eq x y then ys else y : deleteBy eq x ys
deleteBy0 ys y eq x True = ys deleteBy0 ys y eq x False = y : deleteBy eq x ys
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
((union :: [()] -> [()] -> [()]) :: [()] -> [()] -> [()]) |
import qualified Maybe import qualified Prelude |
|||||||||||||||||||||||||||
deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
|
|||||||||||||||||||||||||||
|
|||||||||||||||||||||||||||
elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
|
|||||||||||||||||||||||||||
nubBy :: (a -> a -> Bool) -> [a] -> [a]
|
|||||||||||||||||||||||||||
union :: Eq a => [a] -> [a] -> [a]
|
|||||||||||||||||||||||||||
unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
|
import qualified List import qualified Prelude |
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
((union :: [()] -> [()] -> [()]) :: [()] -> [()] -> [()]) |
import qualified Maybe import qualified Prelude |
|||||||||||||||||||||||||||
deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
|
|||||||||||||||||||||||||||
|
|||||||||||||||||||||||||||
elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
|
|||||||||||||||||||||||||||
nubBy :: (a -> a -> Bool) -> [a] -> [a]
|
|||||||||||||||||||||||||||
union :: Eq a => [a] -> [a] -> [a]
|
|||||||||||||||||||||||||||
unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
|
import qualified List import qualified Prelude |
nubBy' [] vy = [] nubBy' (y : ys) xs
| elem_by eq y xs
= nubBy' ys xs | otherwise
= y : nubBy' ys (y : xs)
nubBy' [] vy = nubBy'3 [] vy nubBy' (y : ys) xs = nubBy'2 (y : ys) xs
nubBy'1 y ys xs True = nubBy' ys xs nubBy'1 y ys xs False = nubBy'0 y ys xs otherwise
nubBy'0 y ys xs True = y : nubBy' ys (y : xs)
nubBy'2 (y : ys) xs = nubBy'1 y ys xs (elem_by eq y xs)
nubBy'3 [] vy = [] nubBy'3 wz xu = nubBy'2 wz xu
undefined
| False
= undefined
undefined = undefined1
undefined0 True = undefined
undefined1 = undefined0 False
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
((union :: [()] -> [()] -> [()]) :: [()] -> [()] -> [()]) |
import qualified Maybe import qualified Prelude |
|||||||||||||||||||||||||||||||||||||||||||||
deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
|
|||||||||||||||||||||||||||||||||||||||||||||
|
|||||||||||||||||||||||||||||||||||||||||||||
elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
|
|||||||||||||||||||||||||||||||||||||||||||||
nubBy :: (a -> a -> Bool) -> [a] -> [a]
|
|||||||||||||||||||||||||||||||||||||||||||||
union :: Eq a => [a] -> [a] -> [a]
|
|||||||||||||||||||||||||||||||||||||||||||||
unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
|
import qualified List import qualified Prelude |
nubBy' l [] where
nubBy' [] vy = nubBy'3 [] vy nubBy' (y : ys) xs = nubBy'2 (y : ys) xs
nubBy'0 y ys xs True = y : nubBy' ys (y : xs)
nubBy'1 y ys xs True = nubBy' ys xs nubBy'1 y ys xs False = nubBy'0 y ys xs otherwise
nubBy'2 (y : ys) xs = nubBy'1 y ys xs (elem_by eq y xs)
nubBy'3 [] vy = [] nubBy'3 wz xu = nubBy'2 wz xu
nubByNubBy'3 xv [] vy = [] nubByNubBy'3 xv wz xu = nubByNubBy'2 xv wz xu
nubByNubBy'0 xv y ys xs True = y : nubByNubBy' xv ys (y : xs)
nubByNubBy' xv [] vy = nubByNubBy'3 xv [] vy nubByNubBy' xv (y : ys) xs = nubByNubBy'2 xv (y : ys) xs
nubByNubBy'1 xv y ys xs True = nubByNubBy' xv ys xs nubByNubBy'1 xv y ys xs False = nubByNubBy'0 xv y ys xs otherwise
nubByNubBy'2 xv (y : ys) xs = nubByNubBy'1 xv y ys xs (elem_by xv y xs)
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
(union :: [()] -> [()] -> [()]) |
import qualified Maybe import qualified Prelude |
|||||||||
deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
|
|||||||||
|
|||||||||
elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
|
|||||||||
nubBy :: (a -> a -> Bool) -> [a] -> [a]
|
|||||||||
|
|||||||||
|
|||||||||
|
|||||||||
|
|||||||||
|
|||||||||
union :: Eq a => [a] -> [a] -> [a]
|
|||||||||
unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
|
import qualified List import qualified Prelude |
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
new_nubByNubBy'(:(@0, xw411), @0) → new_nubByNubBy'(xw411, @0)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDP
new_deleteBy(xw10, :(xw90, xw91), bb) → new_deleteBy0(xw91, xw90, xw10, new_esEs(xw10, xw90, bb), bb)
new_deleteBy0(xw17, xw18, xw19, False, ba) → new_deleteBy(xw19, xw17, ba)
new_esEs(xw10, xw90, app(app(app(ty_@3, cb), cc), cd)) → error([])
new_esEs(xw10, xw90, ty_Double) → error([])
new_esEs(xw10, xw90, ty_Integer) → error([])
new_esEs(xw10, xw90, ty_Ordering) → error([])
new_esEs(xw10, xw90, app(ty_[], ca)) → error([])
new_esEs(xw10, xw90, app(app(ty_@2, bg), bh)) → error([])
new_esEs(xw10, xw90, app(ty_Ratio, bf)) → error([])
new_esEs(xw10, xw90, ty_Char) → error([])
new_esEs(xw10, xw90, ty_Bool) → error([])
new_esEs(@0, @0, ty_@0) → True
new_esEs(xw10, xw90, app(app(ty_Either, bd), be)) → error([])
new_esEs(xw10, xw90, ty_Float) → error([])
new_esEs(xw10, xw90, app(ty_Maybe, bc)) → error([])
new_esEs(xw10, xw90, ty_Int) → error([])
new_esEs(x0, x1, ty_Double)
new_esEs(x0, x1, app(ty_Ratio, x2))
new_esEs(x0, x1, ty_Ordering)
new_esEs(x0, x1, ty_Int)
new_esEs(x0, x1, ty_Integer)
new_esEs(x0, x1, app(app(ty_Either, x2), x3))
new_esEs(x0, x1, ty_Char)
new_esEs(x0, x1, ty_Bool)
new_esEs(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs(x0, x1, ty_Float)
new_esEs(x0, x1, app(app(ty_@2, x2), x3))
new_esEs(x0, x1, app(ty_Maybe, x2))
new_esEs(x0, x1, app(ty_[], x2))
new_esEs(@0, @0, ty_@0)
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
new_foldl(xw9, xw10, :(xw110, xw111), ba) → new_foldl(new_flip(xw9, xw10, ba), xw110, xw111, ba)
new_esEs(xw10, xw90, ty_Double) → error([])
new_esEs(xw10, xw90, app(app(app(ty_@3, cb), cc), cd)) → error([])
new_esEs(xw10, xw90, ty_Integer) → error([])
new_esEs(xw10, xw90, ty_Ordering) → error([])
new_esEs(xw10, xw90, app(app(ty_@2, bg), bh)) → error([])
new_deleteBy00(xw17, xw18, xw19, False, bb) → :(xw18, new_deleteBy1(xw19, xw17, bb))
new_esEs(xw10, xw90, app(ty_[], ca)) → error([])
new_esEs(xw10, xw90, app(ty_Ratio, bf)) → error([])
new_deleteBy00(xw17, xw18, xw19, True, bb) → xw17
new_esEs(xw10, xw90, ty_Char) → error([])
new_esEs(xw10, xw90, ty_Bool) → error([])
new_deleteBy1(xw10, :(xw90, xw91), ba) → new_deleteBy00(xw91, xw90, xw10, new_esEs(xw10, xw90, ba), ba)
new_esEs(@0, @0, ty_@0) → True
new_flip(xw9, xw10, ba) → new_deleteBy1(xw10, xw9, ba)
new_esEs(xw10, xw90, app(app(ty_Either, bd), be)) → error([])
new_esEs(xw10, xw90, ty_Float) → error([])
new_esEs(xw10, xw90, app(ty_Maybe, bc)) → error([])
new_esEs(xw10, xw90, ty_Int) → error([])
new_deleteBy1(xw10, [], ba) → []
new_esEs(x0, x1, ty_Double)
new_esEs(x0, x1, app(ty_Ratio, x2))
new_deleteBy1(x0, [], x1)
new_esEs(x0, x1, ty_Ordering)
new_deleteBy1(x0, :(x1, x2), x3)
new_esEs(x0, x1, ty_Int)
new_esEs(x0, x1, app(app(ty_Either, x2), x3))
new_flip(x0, x1, x2)
new_esEs(x0, x1, ty_Integer)
new_esEs(x0, x1, ty_Char)
new_esEs(x0, x1, ty_Bool)
new_esEs(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs(x0, x1, ty_Float)
new_esEs(x0, x1, app(ty_Maybe, x2))
new_esEs(x0, x1, app(app(ty_@2, x2), x3))
new_esEs(x0, x1, app(ty_[], x2))
new_deleteBy00(x0, x1, x2, False, x3)
new_deleteBy00(x0, x1, x2, True, x3)
new_esEs(@0, @0, ty_@0)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
new_psPs(:(xw80, xw81), xw9, xw10, xw11, ba) → new_psPs(xw81, xw9, xw10, xw11, ba)
From the DPs we obtained the following set of size-change graphs: